\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$(?($\mathbb{N}\rightarrow$(IdLnk + Id)))), $v$:($i$:Id$\rightarrow$M($i$).(timed)state),\+
\\[0ex]${\it dec}$:($i$,$a$:Id$\rightarrow\mathbb{N}\rightarrow$M($i$).state$\rightarrow$(?if $a$ $\in$ dom(M($i$).prob) then Outcome else Void fi )),
\\[0ex]${\it discrete}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$).
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ d{-}feasible{-}discrete($D$;${\it discrete}$)
\\[0ex]$\Rightarrow$ ($\forall$$i$, $x$:Id. ($\uparrow$(${\it discrete}$($i$,$x$))) $\Rightarrow$ constant\_function($v$($i$,$x$);$\mathbb{Q}$;M($i$).ds($x$)))
\\[0ex]$\Rightarrow$ \=($\forall$$i$:Id.\+
\\[0ex](\=$\forall$$l$:IdLnk.\+
\\[0ex](destination($l$) = $i$)
\\[0ex]$\Rightarrow$ ($\uparrow$M(source($l$)) sends on link $l$)
\\[0ex]$\Rightarrow$ \=(($\uparrow$isl(${\it sched}$($i$)))\+
\\[0ex]c$\wedge$ \=($\forall$$t$:$\mathbb{N}$.\+
\\[0ex]$\exists$\=${\it t'}$:$\mathbb{N}$\+
\\[0ex](($t$ $\leq$ ${\it t'}$) \& (($\uparrow$isl(outl(${\it sched}$($i$))(${\it t'}$))) c$\wedge$ (outl(outl(${\it sched}$($i$))(${\it t'}$)) = $l$))))))
\-\-\-\-\\[0ex]\& (\=$\forall$$a$:Id.\+
\\[0ex]$a$ in dom(M($i$).pre)
\\[0ex]$\Rightarrow$ \=(($\uparrow$isl(${\it sched}$($i$)))\+
\\[0ex]c$\wedge$ \=($\forall$$t$:$\mathbb{N}$.\+
\\[0ex]$\exists$\=${\it t'}$:$\mathbb{N}$\+
\\[0ex](($t$ $\leq$ ${\it t'}$)
\\[0ex]\& (($\uparrow$($\neg_{b}$isl(outl(${\it sched}$($i$))(${\it t'}$)))) c$\wedge$ (outr(outl(${\it sched}$($i$))(${\it t'}$)) = $a$)))))))
\-\-\-\-\-\\[0ex]$\Rightarrow$ FairFifo
\end{tabbing}